Inference at * 1 
Iof proof for Lemma absval eq:



1. x : 
2. y : 
  (|x| = |y|)  x =  y 

latex

 by Unfold `absval` 0 

latex

 1: 

 1:   (if 0 z x then x else -x fi  = if 0 z y then y else -y fi )  x =  y
 .

Definitions

|i|